With reference to FIG. 1, an integrated circuit to implement integer division 100 (which may be referred to herein as an integer divider) receives as inputs a numerator N and a denominator D, performs (via hardware logic) the operation N divided by D
      (          i      .      e      .                          ⁢              N        D              )    ,and outputs the quotient q and the remainder r of the operation, wherein N=D*q+r, |r|<|D|, and N, D, q and r are integers. As is known to those of skill in the art, when the numerator N and the denominator D are both positive, the quotient q is the number of times the denominator D may be subtracted from the numerator N before the result of the subtraction is negative; and the remainder r is the amount left over after subtracting the denominator D the quotient q number of times from the numerator N. For example, if the numerator N is 26 and the denominator D is 11 then the quotient q of the operation
      N    D    =      26    11  is 2, and the remainder r is 4.
To generate an integrated circuit to implement integer division 100 an integrated circuit hardware design is generated which describes the structure and function of an integrated circuit to implement integer division. The integrated circuit hardware design is then tested, or verified, to ensure that an integrated circuit manufactured in accordance with the integrated circuit hardware design will behave as expected. Once the integrated circuit hardware design has been verified the integrated circuit hardware design is processed at an integrated circuit manufacturing system to generate an integrated circuit in accordance with the integrated circuit hardware design.
An integrated circuit hardware design may be verified, for example, by formal verification or simulation-based verification. Formal verification is a systematic process that uses a mathematical model of the integrated circuited design and mathematical reasoning to verify an integrated circuit hardware design. In contrast, simulation-based verification is a process in which an integrated circuit hardware design is tested by applying stimuli to an instantiation of the integrated circuit hardware design and monitoring the output of the instantiation of the integrated circuit hardware design in response to the stimuli.
Formal verification can improve controllability as compared to simulation based verification. Low controllability occurs when the number of simulation test signals or vectors required to thoroughly simulate a hardware design becomes unmanageable. For example, a 32-bit comparator requires 264 test vectors (e.g. stimulus). This would take millions of years to verify exhaustively by simulation based verification. By performing formal verification, the 32-bit comparator can be verified in less than a minute.
While formal verification can provide advantages over simulation-based verification, integrated circuit hardware designs to implement integer division have been difficult to verify using formal verification.
The embodiments described below are provided by way of example only and are not limiting of implementations which solve any or all of the disadvantages of known methods and systems for verifying an integrated circuit hardware design to implement integer division.